00100	GIVEAX(IGR99,(∀ R)(∀ P)(AIW(P,R) ≡ SCORDERING R ∧ Pε(DOMAIN R → TV)
00200	(∀ S)(ASCENDSEQ(R,S) ⊃ (β(P,UU)=T ∧ (∀ N)(NεI0 ⊃
00300	β(P,β(S,N))=T) ⊃ β(P,LUB(R,S))=T)	 )));
00400	
00500	GIVEAX(IGR101,(∀ R1)(∀ R2)(∀ F)(∀ G)(∀ P)(SCORDERING R1
00600	∧ SCORDERING R2 ∧ FεDOMAIN(R1→→R2) ∧ GεDOMAIN(R1→→R2) 
00700	∧ Pε(DOMAIN R1 → TV)
00800	∧ (∀ X)(Xε(DOMAIN R1) ⊃ (β(P,X)=T ⊃ ββ(β(F,X),R2,β(G,X)))
00900	⊃ AIW(P,R1)));